package datatableaux;



import utils.io.KBAccess;
import kb.ABox;
import kb.DescriptionLogicsKB;
import kb.TBox;
import entities.Assertion;
import entities.ConceptAssertion;
import entities.Individual;
import entities.concept.Concept;
import entities.concept.NotConcept;
import entities.vocabulary.Display;


/**
 * 
 * This class provides interfaces to the basic operations of the reasoner.
 * Work flow:
 * get the tbox TB by parsing a file/stream: getTBox(String fileName);
 * get the subsumption test concept Con, e.g., A under C?, from a file/stream: getSubsumptionTest(String fileName);
 * call subsumes(Con, TB) to see if Con holds w.r.t. TB.
 * add more axioms: addAxioms(String fileName, TBox tb),  to the tbox as you wish, then call subsumes(Con, TB) again!
 * 
 *  you don't need to compile the tbox directly, when the subsumption is tested, it will be re-compiled automatically.
 * @author J.W.Wu
 *
 */
public class Reason {
	//private final static boolean ABOX_REASONING = true;
	private boolean verbose;
	
	public Reason(){
		//default: verbose is true;
		verbose = true;
	}
	
	public Reason(boolean verbose){
		this.verbose = verbose;
	}

//	private Concept getSubsumptionTest(String fileName) throws IOException{
//		Concept sat = null;
//		if(verbose){
//			System.out.println("Subsumption to test:\n--------");
//		}
//		HashSet<Axiom> satConcepts = KBAccess.getTBox(fileName);
//		if(satConcepts.size()==1){
//			sat = satConcepts.iterator().next().getConcept();
//		}else{
//			if(verbose)
//				System.out.println("This interface allows only one subsumption test per request.");
//			}
//		return sat;
//	}
	
	
	/**
	 * Check if {T, A} |= C -> D. In our reasoner, this is the same as {T, A} U {a:C} |= {a:D} for some anonymous a.
	 */
	public boolean TBoxSubsumptionCheck(Concept lhs, Concept rhs, DescriptionLogicsKB kb){
//		Individual ind = Individual.getAnonIndividual();
//		ConceptAssertion ca = new ConceptAssertion(ind, lhs);
//		ab.insertAssertions(ca);
//		ConceptAssertion ast = new ConceptAssertion(ind, rhs);
//		boolean ret = ABoxConsistentWRTTBox(true, tb, ab, ast);
//		//clean what's been added: ca, ind
//		ab.rmAssertions(ca);
//		ab.getABoxIndividuals().remove(ind);
//		return ret;
		Individual ind = Individual.getAnonIndividual();
		ConceptAssertion ca = new ConceptAssertion(ind, lhs);
		ABox newab = null;
		if(kb!=null && kb.getAbox() != null){
			newab = kb.getAbox().deepcopyOfThisABox();
			newab.insertAssertions(ca);
		}else{
			newab = KBAccess.newABoxInstance(ca);
		}
		TBox tb= null;
		if(kb !=null){
			tb = kb.getTbox();
		}
		ConceptAssertion ast = new ConceptAssertion(ind, rhs);
		boolean ret = ABoxConsistentWRTTBox(true, tb, newab, ast);
		return ret;
	}
	
	/**
	 * Check if {T, A} U {a:C} |= {a:D} for some named instance a.
	 * @param lhs
	 * @param rhs
	 * @param tb
	 * @param ab
	 * @return
	 */
	public boolean ABoxUnionAssertionEntailAssertionCheck(Assertion lhs, Assertion rhs,DescriptionLogicsKB kb){
//		ab.insertAssertions(lhs);
//		boolean ret = ABoxConsistentWRTTBox(true, tb, ab, rhs);
//		ab.rmAssertions(lhs);
//		return ret;
		//System.out.println("start test: "+lhs +" -> "+rhs);
		ABox newab = null;
		if(kb!= null && kb.getAbox() != null){
			newab = kb.getAbox().deepcopyOfThisABox();
			newab.insertAssertions(lhs);
		}else{
			newab = KBAccess.newABoxInstance(lhs);
		}
		TBox tb = null;
		if(kb!= null){
			tb = kb.getTbox();
		}
		boolean ret = ABoxConsistentWRTTBox(true, tb, newab, rhs);
		//System.out.println("exit test: "+lhs +" -> "+rhs+". " + ret);
		return ret;
	}
	

	
	/*
	 * @param entail: true if check if A |= ast, i.e., checking entailment problem.
	 * @param tb: optional, a general tbox with axioms, can be null
	 * @param ab: optional, the initial abox with all assertions, can be null
	 * @param ast: the assertion to be tested of the form a:C
	 * Return true if a:C causes inconsistency, false otherwise.
	 */
	public boolean ABoxConsistentWRTTBox(boolean entail, TBox tb, ABox ab, Assertion ast){
		String s = "\n\n";
		ab.cleanUp();
		if(tb != null){
			tb.compileTBox();
		}
		if(entail){
			if(ast != null && ast instanceof ConceptAssertion){
				s += "Testing if ("+Display.TBOXUNICODE+", "+Display.ABOXUNICODE+") "+Display.MODELSUNICODE+" "+ ast.toString();
				ConceptAssertion cast = (ConceptAssertion) ast;
				//change a:C into a:~C
				ast = new ConceptAssertion(cast.getIndividual(), new NotConcept(cast.getConcept()));
			}else{
				System.err.println("Unable to check entailment of a role assertion: reasoner to be updated.");
				throw new RuntimeException();
			}	
		}		
		DataCompletion dc = new DataCompletion(tb,ab,ast);
		boolean cons = dc.checkABoxConsistency();
		if(entail){
			if(!cons){
				s += "\nGiven assertion is entailed by (T, A).";
			}else{
				s += "\nGiven assertion is NOT entailed by (T, A).";
			}
			if(verbose) System.out.println(s);
			return !cons;
		}else{
			s += "Checking ABox "+ Display.ABOXUNICODE+ " consistency ... ...";
			if(cons){
				s += "\nABox is Consistent!";
			}else{	
				s += "\nABox is inconsistent.";
			}
			if(verbose) System.out.println(s);
			return cons;
		}
	}
	
//	/**
//	 * @deprecated
//	 * @param c: the concept to bes tested. If you provide an inclusion A -> B, this concept should be (not A or B).
//	 * <br> In our case, the syntax is (or (not A) B).
//	 * @param tb: the tbox that contains all the axioms of the form (implies C D). 
//	 * @return true if this subsumption holds w.r.t. the given tbox.
//	 */
//	public boolean subsumes(Concept c, TBox tb){
//		if(ABOX_REASONING){
//			//use abox consistency checking, i.e., K |= C iff  a:C causes inconsistency, where a is a fresh anonymous individual.
//			ConceptAssertion ca = new ConceptAssertion(Individual.getAnonIndividual(), c);
//			//the ABox must be the one loaded for indexing!
//			return this.ABoxConsistentWRTTBox(true, tb, null, ca);
//		}
//		
//		//To see if C is valid, we show if ~C is unsat!
//		String s = "";
//		if(c == null){
//			System.out.println("No subsumption to test: exit abnormally.");
//			return true;
//		}
//		Concept test = Simplification.NNF(new NotConcept(c), false);
//		s += "Testing if "+ test.toString()+" is unsat...\n";
//		if(tb != null){
//			tb.compileTBox();
//		}
//		Completion comp = new Completion(test, tb);
//		boolean sat = comp.isSatisfiable();
//		s += "Subsumption Concept " + c.toString();
//		if(sat){
//			//C is not valid
//			s += " does NOT hold.";
//		}else{
//			//C is valid as the concept test is unsat!
//			s += " holds w.r.t. this TBox.";
//		}
//		if(verbose) System.out.println(s);
//		return !sat;
//	}
	
	

}
